Nuprl Definition : Reffect-discrete
11,40
postcript
pdf
Reffect-discrete(
A
) == case Reffect-f(
A
) of inl(
f
) => tt | inr(
f
) => ff
latex
Definitions
ff
,
tt
,
Reffect-f(
x1
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
FDL editor aliases
Reffect-discrete
origin